x, y:MaName. Dec(x = y) 

latex

Definitions	t  T, x:A. B(x), x:AB(x), s = t, Dec(P), maname-deq(), MaName, eqof(d), f(a), P  Q, P  Q, b, P & Q, P  Q, Type, , x:A  B(x)
Lemmas	decidable functionality, assert wf, decidable assert, eqof wf, deq property, maname-deq wf, MaName wf